Inference at * 1 
Iof proof for Lemma primrec add:



1. T : Type
2. m : 
3. b : T
4. c : {0..(0+m)}TT
  primrec(0+m;b;c) = primrec(0;primrec(m;b;c);i,t. c(i+m,t)) 

latex

 by Reduce 0 

latex

 1: 

 1:   primrec(0+m;b;c) = primrec(m;b;c)
 .

Definitions

tt, (i = j), if b then t else f fi , Y, primrec(n;b;c)